Notes (Week 7 Wednesday)

Question on notice from W7 Monday:

Q: Is the negation of a safety property a liveness property and vice
versa?

A: No

  The universe 𝓤  (the set of all behaviours)
    is both a safety and a liveness property

  The ∅ (the set of no behaviours)

    ...is a safety property, but not a liveness property.

Find an automaton that accepts words where every
  odd symbol is b
 Think about what properties of the word so far
  we need to track.

 - Have we seen an even or odd number of symbols so far?
 - Have we seen an a in an odd position yet?


  q0: I have seen an even number of symbols,
       and no malplaced a so far
  q1: I have seen a malplaced a
  q2: I have seen an odd number of symbols,
       and no maplaced a so far

            a,b
           <----
 -->  (q0) ----> (q2)
      |    b
      |
      | a
      ∨
     q1 --\
       ∧  | a,b 
       |  |
       \--/